package ch.epfl.lara.matcheck.verify.transform;

import ch.epfl.lara.matcheck.ast._



object TreeExpr2Formula extends AbstractConversion2Formula { 
  
  def apply(expr: Expr): (Formula,String) = {
    generated_names = Nil  
    Convert(expr)
  }
  
  

  def apply(tpe: TypeTree): Set = Convert(tpe)
  
  private object Convert {
    import ch.epfl.lara.matcheck.util.Substitute
  
    implicit def packres(e: E): (Formula,String) = pack(e)
    
    implicit def string2elem(s: String): Element = Element(s)
    
    
    private def pack(e: E): (Formula,String) = {
      val fresh = freshName(e.makeName)
      (Eq(fresh,e),fresh)
    }
    
  
  
    def apply(expr: Option[Expr]): (Formula,String) = expr match {
      case None => Tru
      case Some(expr) => this(expr)
    }
  
    def apply(expr: Expr): (Formula,String) = expr match {
      case ObjectId(name) => 
        val static_name = "object__"+name.getName
        val fresh = freshName("object")
        (Eq(fresh,static_name),fresh)
        
      case Ident(name)  => Element(name.getName) 
      case True         => Tru
      case False        => Flse
      case Number(n)    => Const(n) 
      case StringLit(s) => StringLit0(s)

  
      case IsInstanceOf(e,tpe) =>
        val (lhs,fresh) = this(e)
        val ret = freshName("isinstof")
        (And(lhs,Equality(ret,In(fresh,this(tpe)))),ret)
    
      case New(klass,args) =>
        val fresh = freshName("new")
        var left: Formula = In(fresh,Set(klass.getName))
        var xs: List[String] = Nil
      
        for(arg<-args) {
          val (l,res) = this(arg)
          left = And(left,l)
          xs = res :: xs
        }
      
        for((field,value)<-klass.getSym.allFields.zip(xs)) {
          val name = klass.getName + "_getField_" +field.getName
          left = And(left,Eq(Function(name,List(fresh)),value))
        }
      
        klass.getSym.invariant match {
          case None => ()
          case Some(inv) => left = And(left,inv)
        }
      
        (left,fresh)
      
      case Call(obj,method,args) => 
        val (l,this_name) = this(obj)
        var lhs: Formula = l
        

        val args_fresh = for(arg<-args) yield {
          val (a_lhs,a_fresh) = this(arg)
          lhs = And(lhs,a_lhs)        
          a_fresh
        }
    
        val res = freshName("call")
        var name: String = "call_"+method.getName
        
        if(method.getSym != null) {
          val msym @ MethodSymbol(mname,params,resTpe,ppc) = method.getSym
          name = mname.getSym.getName+"_"+mname
      
          val env = ("this",this_name) :: (msym.RES,res) :: params.map(_._1).zip(args_fresh)
      
          val postcondition = ppc match {
            case None => Tru
            case Some((_,post)) => Substitute(env,post) 
          }
          lhs = And(lhs,postcondition)
        }
        
        val call = Eq(res,Function(name,this_name :: args_fresh.map(string2elem(_))))
        
        (And(lhs,call),res)
   
      case Select(obj,field) => 
        val (lhs,objName) = this(obj)
        if(field.getSym != null) {
          val name = field.getSym.name.getSym.getName+"_getField_"+field.getName
          val fresh = freshName("deref")
          (And(lhs,Eq(Function(name,List(objName)),fresh)),fresh)
        } else 
          (lhs,objName) 
       
      case &&(left,right) => packBoolExpr(And, left, right)
      case ||(left,right) => packBoolExpr(Or, left, right)  
      case +(left,right) => packArithExpr(Plus, left,right)
      case -(left,right) => packArithExpr(Minus, left,right)  
      case /(left,right) => packArithExpr(Div, left,right)
      case %(left,right) => packArithExpr(Mod, left,right)
      case *(left,right) => packArithExpr(Prod, left,right)
      case <(left,right)  => packCmpExpr(Less,left,right)
      case <=(left,right) => packCmpExpr(LessEq,left,right)
      case ==(left,right) => packCmpExpr(Eq,left,right)
      case !(f) => 
        val (lhs,fresh) = this(f)
        val neg = freshName("neg")
        val eq = Equality(neg,Neg(fresh))
        (And(lhs,eq),neg)
    
      case If(cond,then,elze) =>
        val (condition,res_if) = this(cond)
        val(then_cond,res_then) = this(then)
        val(elze_cond,res_elze) = this(elze)
        val res = freshName("if")
        val eq = Equality(res,And(Imply(res_if,res_then),Imply(Neg(res_if),res_elze)))      
        (And(And(condition,And(then_cond,elze_cond)),eq),res)
       
      case Match(scrutinee,tpe,cases) =>
        val (lhs_scrut,res_scrut) = this(scrutinee)
        val scrut_tpe = Equality(freshName("scrutinee"),In(res_scrut,this(tpe)))
        val scrutinee_axiom = And(lhs_scrut,scrut_tpe)
        var left = scrutinee_axiom
        var cases_res: List[Formula] = Nil
       
        for(CaseDef(_,pattern,guard,body)<-cases) {
        
          val Imply(p_lhs,p_rhs) = Pattern2Formula(res_scrut,pattern)
          append_names(Pattern2Formula.generated_fresh_names)
          
          val (guard_lhs,guard_res) = this(guard)
          
          val (body_lhs,body_res) = this(body)
        
          val fresh = freshName("case")
          val case2formula = And(And(p_rhs,guard_res),
                                 And(body_res,
                                     cases_res.foldLeft[Formula](Tru)((l,r) => And(l,Neg(r)))))
        
          left = And(And(And(left,p_lhs),And(guard_lhs,body_lhs)),Equality(fresh,case2formula))
                                             
          cases_res = fresh :: cases_res
        }
      

        val result = freshName("pm")
        var pm: Formula = Tru
        if(cases_res.length == 0) () 
        else if(cases_res.length == 1) pm = cases_res.head
        else for(i<-List.range(0,cases_res.length-1);j<-List.range(i+1,cases_res.length)) {
          pm = And(pm,Neg(And(cases_res(i),cases_res(j))))  
        }
      
        val pm_res = Equality(result,
                            And(pm,
                            cases_res.foldLeft[Formula](Flse)((l,r) => Or(l,r))))
                             
        (And(left,pm_res),result)
     
    }
  
  
    private def packBoolExpr(op: (Formula,Formula)=>Formula, left: Expr, right: Expr): (Formula,String) = {
      val (form_llhs,el_l) = this(left)
      val (form_rlhs,el_r) = this(right)
      val fresh = freshName("bop")
      val res = Equality(fresh,op(el_l,el_r))
      (And(And(form_llhs,form_rlhs),res),fresh)
    }
  
    private def packCmpExpr(op: (E,E)=>Atom0, left: Expr, right: Expr): (Formula,String) = {
      val (form_llhs,el_l) = this(left)
      val (form_rlhs,el_r) = this(right)
      val fresh = freshName("cmp")
    
      val res = Equality(fresh,op(el_l,el_r))
      (And(And(form_llhs,form_rlhs),res),fresh)
    }
  
  
    private def packArithExpr(op: (Term0,Term0)=>Term0, left: Expr, right: Expr): (Formula,String) = {
      val fresh = freshName("aop")
      val (form_llhs,el_l) = this(left)
      val (form_rlhs,el_r) = this(right)
      (And(And(form_llhs,form_rlhs),Eq(fresh,op(IntVar(el_l),IntVar(el_r)))),fresh)
    }
    
    def apply(tpe: TypeTree): Set = Set(tpe.toString)
  }
}

